Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    le(0,y)  → true
2:    le(s(x),0)  → false
3:    le(s(x),s(y))  → le(x,y)
4:    minus(x,0)  → x
5:    minus(s(x),s(y))  → minus(x,y)
6:    mod(0,y)  → 0
7:    mod(s(x),0)  → 0
8:    mod(s(x),s(y))  → if_mod(le(y,x),s(x),s(y))
9:    if_mod(true,x,y)  → mod(minus(x,y),y)
10:    if_mod(false,s(x),s(y))  → s(x)
There are 6 dependency pairs:
11:    LE(s(x),s(y))  → LE(x,y)
12:    MINUS(s(x),s(y))  → MINUS(x,y)
13:    MOD(s(x),s(y))  → IF_MOD(le(y,x),s(x),s(y))
14:    MOD(s(x),s(y))  → LE(y,x)
15:    IF_MOD(true,x,y)  → MOD(minus(x,y),y)
16:    IF_MOD(true,x,y)  → MINUS(x,y)
The approximated dependency graph contains 3 SCCs: {11}, {12} and {13,15}.
Tyrolean Termination Tool  (0.13 seconds)   ---  May 4, 2006